Nuprl Lemma : Q-R-pre-preserving-compose 11,40
es:ES, P1, P2:(E), Q1, Q2, Q3:(EE), f1:({e:E| P1(e)} {e:E| P2(e)} ),
f2:({e:E| P2(e)} E).
f1 is Q2-Q3-pre-preserving on P1
 f2 is Q1-Q2-pre-preserving on P2
 f2 o f1 is Q1-Q3-pre-preserving on P1 
latex

Definitionst  T, f(a), x:A. B(x), x:AB(x), E, {x:A| B(x)} , , P  Q, x.A(x), Type, ES, f is Q-R-pre-preserving on P, f o g

origin